The present invention generally relates to hardware and software formal verification systems and methods, and more specifically, to providing model checking and symbolic simulation using a hardware description language.
Formal verification is widely used to verify or identify correctness of a software or hardware design. Correctness, in general, is a determination that the design is equivalent to a specification. The specification commonly represents expected responses of the design exposed to predetermined stimuli, e.g., test vector sequences. The design and specification can be represented in multiple forms of abstractions.
However, it is often difficult to construct an abstract behavior to a given specification without an exhaustive construction of the design's state space. Furthermore, verification of the design often requires that a large part of the state space of the design be generated, as the design is exhaustively checked for all possible computation scenarios. Since, the number of states may grow exponentially relative to the number of components in the design, verifying the design often becomes a resource-consuming operation, both in terms of memory and processor utilization and time. Thus, there are often a limit to the size of the design that may be verified.
Furthermore, at times, verification of designs requires multiple iterative and interactive input from a designer making the process more arduous and time consuming. Also, integration of the verification within the design process becomes difficult and less “automatic”. Moreover, if the verification of the design result in the design not being verified, then providing a “debug” trace to enable a designer to locate the error would be helpful. Also, providing this “debug” information early in the design cycle allows the correction of these errors to be less expensive in terms of time and money.